T, A:Type, f:(AT), l:IdLnk.
Normal(A)  Normal(T)  es.locl("b") sends ["tg",f{AT}("done")] on link l once 

latex

Definitions

Id, P  Q, x:A. B(x), "$x", Prop, x. t(x), t  T, 1of(t), ||as||, Top, nth_tl(n;as), once-realizable, l[i], b, DeclaredType(ds;x), if b t else f fi, send_onceR{$done:ut2, $tg:ut2, $b:ut2, $done1:ut2}(T; A; f; l), {i..j}, i  j < k, true, s.x, i<j, onceR{$a:ut2, $done:ut2}(i), A, False, Y, false, ij, P & Q, implies-es-real, es-realizer(p), hd(l), AB, tl(l), A & B, usends1-p-realizable, Normal(T), locl(a) sends [tg,f{AT}(x)] on link l once, x:A. B(x), True, x when e, T, x(s), State(ds), b, isrcv(k), locl(a), isl(x), ES, e@i.P(e), usends1-p(es;ds;k;T;l;tg;B;f), @i locl(a) occurs once, e@i. P(e), {T}, State(ds)

Lemmas

normal-type wf, send onceR wf, IdLnk wf, implies-es-real, send onceR feasible, event system wf, send-once-p wf, R-consistent wf, deq wf, es-realizer wf, es-real-implies, le wf, fpf-cap-single1, R-sub-Rlist, Rinit wf, fpf-cap-single, Id wf, lsrc wf, es-real wf, Rsends wf, eqof eq btrue, btrue wf, subtype rel self, R-sub-implies, Rlist wf, Rframe wf, Reffect wf, Rpre wf, once-p wf, bool wf, fpf-single wf, select member, id-deq wf, lnk wf, tagof wf, usends1-p wf, ldst wf, normal-ds-single, it wf, es-val wf, es-kind wf, es-vartype wf, es-when wf, es-kind-rcv, rcv wf, es-sender wf, es-E wf, squash wf, true wf, assert wf, es-isrcv wf, es-loc wf